Establishing Object Invariants with Delayed Types. Manuel Fähndrich, Songtao Xia.
Mainstream object-oriented languages such as C# and Java provide an initializationmodel for objects that does not guarantee programmer controlled initialization of fields. Instead, all fields are initialized to default values (0 for scalars and null for non-scalars) on allocation. This is in stark contrast to functional languages, where all parts of an allocation are initialized to programmer-provided values. These choices have a direct impact on two main issues: 1) the prevalence of null in object oriented languages (and its general absence in functional languages), and 2) the ability to initialize circular data structures. This paper explores connections between these differing approaches and proposes a fresh look at initialization. Delayed types are introduced to express and formalize prevalent initialization patterns in object-oriented languages.
It's interesting to note that in Ada type definitions can contain initializers (i.e., initialization expressions), partly because constructors were introduced into the language only in the second revision of the language (Ada95).
A functional correspondence between evaluators and abstract machines by Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard, 2003.
We bridge the gap between functional evaluators and abstract machines for the lambda-calculus, using closure conversion, transformation into continuation-passing style, and defunctionalization of continuations.
We illustrate this bridge by deriving Krivine's abstract machine from an ordinary call-by-name evaluator and by deriving an ordinary call-by-value evaluator from Felleisen et al.'s CEK machine. The first derivation is strikingly simpler than what can be found in the literature. The second one is new. Together, they show that Krivine's abstract machine and the CEK machine correspond to the call-by-name and call-by-value facets of an ordinary evaluator for the lambda-calculus.
We then reveal the denotational content of Hannan and Miller's CLS machine and of Landin's SECD machine. We formally compare the corresponding evaluators and we illustrate some relative degrees of freedom in the design spaces of evaluators and of abstract machines for the lambda-calculus with computational effects.
I was surprized not to find this paper featured in a story on LtU, as it looks very important both from implementation and understanding points of view.
See also more recent paper by Dariusz Biernacki and Olivier Danvy: From Interpreter to Logic Engine by Defunctionalization, which applies similar ideas in context of Prolog-like language.
VamOz: Visual Abstract Machine for Oz
VamOz is a visual abstract machine executing kernel language programs as defined in the book Concepts, Techniques and Models of Computer Programming by Peter Van Roy and Seif Haridi.
VamOz has been developed by Frej Drejhammar and Dragan Havelka with contributions from Christian Schulte. The idea is to give students a tool with which they can increase their understanding of how the abstract machine computes. VamOz has been used successfully in 2003 in the Datalogi II course taught by Christian Schulte at KTH.
The first annual D Programming Language Conference is being held in Seattle this week.
You can get a taste by following the live blogging here.
Theory and Practice of Constraint Handling Rules, Thom Fruewirth, Journal of Logic Programming, 1994.
Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved.
In this broad survey we cover all aspects of CHR as they currently present themselves. Going from theory to practice, we will define the syntax and semantics of CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers -- both traditional and non-standard ones -- written in the CHR language. Finally we introduce two innovative applications that benefited from being written in CHR.
In the last post, we had some requests for constraint programming, so here you go. Constraint solving programs are often essentially stateful algorithms, and I see CHR as a particularly nice way of handling all that state in a declarative way. (They have a very pretty semantics as proof search in linear logic, too.)
Beyond Pretty-Printing: Galley Concepts in Document Formatting Combinators, Wolfram Kahl. 1999.
Galleys have been introduced by Jeff Kingston as one of the key concepts underlying his advanced document formatting system Lout. Although Lout is built on a lazy functional programming language, galley concepts are implemented as part of that language and defined only informally. In this paper we present a first formalization of document formatting combinators using galley concepts in the purely functional programming language Haskell.
We've talked about functional layout algorithms for mathematics before, so it seems like a good idea to link to a paper about typesetting all the text those formulas are surrounded by.
Status Report: HOT Pickles, and how to serve them, Andreas Rossberg, Guido Tack, and Leif Kornstedt. ML Workshop 2007.
The need for flexible forms of serialisation arises under many circumstances, e.g. for doing high-level inter-process communication or to achieve persistence. Many languages, including variants of ML, thus offer pickling as a system service, but usually in a both unsafe and inexpressive manner, so that its use is discouraged. In contrast, safe generic pickling plays a central role in the design and implementation of Alice ML: components are defined as pickles, and modules can be exchanged between processes using pickling. For that purpose, pickling has to be higher-order and typed (HOT), i.e. embrace code mobility and involve runtime type checks for safety. We show how HOT pickling can be realised with a modular architecture consisting of multiple abstraction layers for separating concerns, and how both language and implementation benefit from a design consistently based on pickling.
The program for CUFP 2007 is now available. The goal of CUFP is to build a community for users of functional programming languages and technology, be they using functional languages in their professional lives, in an open source project (other than implementation of functional languages), as a hobby, or any combination thereof.
This year's offering includes presentations about projects that use Caml, Erlang, Haskell, Scheme, F# and more. Domain specific embedded languages are also mentioned in the abstracts. Some of the presentations deal with projects mentioned here before, such as the Intel IXP network processor but others are new to me and sound quite intriguing.
Some of the people involved with the CUFP workshop are LtU regulars and contributors who may want to add more details and respond to questions or comments.
Taming the IXP network processor, Lal George and Matthias Blume. PLDI 2003.
We compile Nova, a new language designed for writing network processing applications, using a back end based on integer-linear programming (ILP) for register allocation, optimal bank assignment, and spills. The compiler's optimizer employs CPS as its intermediate representation; some of the invariants that this IR guarantees are essential for the formulation of a practical ILP model.
Appel and George used a similar ILP-based technique for the IA32 to decide which variables reside in registers but deferred the actual assignment of colors to a later phase. We demonstrate how to carry over their idea to an architecture with many more banks, register aggregates, variables with multiple simultaneous register assignments, and, very importantly, one where bank- and register-assignment cannot be done in isolation from each other. Our approach performs well in practise--without causing an explosion in size or solve time of the generated integer linear programs.
This is a nice paper showing how to design and compile a small functional language in a high-performance domain with a very irregular underlying machine model.
|
Recent comments
2 weeks 3 days ago
2 weeks 4 days ago
2 weeks 5 days ago
2 weeks 5 days ago
3 weeks 3 days ago
3 weeks 3 days ago
3 weeks 3 days ago
6 weeks 4 days ago
7 weeks 2 days ago
7 weeks 2 days ago